Bls operations rebased #64
Conversation
| msg)) }}); | ||
| }; | ||
|
|
||
| // TODO: Under what conditions is this true? Should probably be done over IETF |
There was a problem hiding this comment.
I think some version of this is proved using an assumption about the high-level spec in hash_to_g2.saw
| hash_to_curve_E1_opt_impl_equiv_ov <- (prove_hash_to_curve_E1_opt_impl_equiv_thm 32 43); | ||
|
|
||
| // TODO: why is this needed here (see prove_hash_to_g1_ov in hash_to_g1.saw)? | ||
| hash_to_curve_e1_impl_thm <- custom_prove_cryptol |
There was a problem hiding this comment.
Could we use blst_hash_to_g1_spec instead so that we get the high-level spec directly?
There was a problem hiding this comment.
Maybe? The reason I used blst_hash_to_g1_impl_spec is that its postcondition is written with llvm_points_to, while blst_hash_to_g1_spec is written with llvm_postcond. The llvm_postcond forms tend to be painful to work with.
core_verify_pk_in_g2 is wip
I don't understand the error that arises otherwise.
nano-o
force-pushed
the
bls_operations_rebased
branch
from
9cca84d
to
2a37a46
Compare
|
@bboston7 can you have a look before we merge it into main? |
| }}; | ||
|
|
||
| // case in which no argument is null and the error condition is false | ||
| let blst_core_verify_pk_in_g1_non_null_spec msg_len dst_len aug_len = do { |
There was a problem hiding this comment.
This will need a NULL aug version at some point.
There was a problem hiding this comment.
okay, will do that in a later PR
No description provided.